theory DesignSpec
imports Main "../GPTEE_Function_Layer/GPTEE_Instantiation"
        
begin

section "Design level specification: data structure"

subsection "Module: IPC driver"


(*we didnt model wirte_msg ,thread, channel and so on*)
type_synonym fifo = int
(*do we need to identify 32 bit or 64 bit
integrete them to int, no need to differ*)
type_synonym fun_id = int
datatype out_result = ZX_OKr | ZX_ERR_INTERNALr
type_synonym out_params = int
datatype RET = ZX_OK | ZX_ERR_INTERNAL
definition zx_channel_call::"bool" where
  "zx_channel_call ≡ True"
datatype ReadSub=zx_mgr|zx_svc

record smc_params =  
             a0::nat (*default to TEESMC_OPTEED_RETURN_CALL_DONE, i.e, 0*)
             a1::nat (*depends on the result of check_Data,default to OPTEE_SMC_RETURN_OK, i.e, 0*)
             a2::nat (*we use to identify data for mgr(5) or svchost(6)*)
             a3::nat(*used ina openSession, stand for returned session id*)
             a4::nat
             a5::nat
             a6::nat
             a7::nat
             u2k::nat
             k2u::nat

(*designed for step 4 of API in TEEC side*)
definition smc_ex_init where 
    "smc_ex_init=⦇a0=0,a1=0,a2=0,a3=0,a4=0,a5=0,a6=0,a7=0,u2k=0,k2u=0⦈"

(*designed for step 4 of API in TEEC side when step4 succeed*)
definition smc_ex_init2 where 
    "smc_ex_init2=⦇a0=0,a1=0,a2=0,a3=0,a4=1,a5=0,a6=0,a7=0,u2k=0,k2u=0⦈"


(*designed for step 2 of API in TEEC side*)
definition smc_ex_init_read where 
    "smc_ex_init_read=⦇a0=0,a1=0,a2=0,a3=0,a4=0,a5=0,a6=0,a7=0,u2k=0,k2u=0⦈"

datatype SMC_ERROR = OPTEE_SMC_RETURN_OK | OPTEE_SMC_RETURN_EBADCMD | OPTEE_SMC_RETURN_EBADADDR

record driver =
    tamgr_fifo::fifo
    svchost_fifo::fifo
    tamgr_data::smc_params
    svchost_data::smc_params
   (* function_id::nat*)

subsection "Main structure"

(*extend more state variable here*)
record StateR=State + IPC_driver::driver

definition abstract_state :: "StateR ⇒ State" ("⇑_" [50]) 
  where "abstract_state r = ⦇current = current r,
                            TAs_state = TAs_state r,
                            REE_state = REE_state r,
                            TEE_state = TEE_state r,
                            system_time = system_time r,  
                            exec_prime = exec_prime r
                           ⦈"

definition abstract_state_rev :: "StateR ⇒ State ⇒ StateR" ("_⇓_" [50])
  where "abstract_state_rev r r' = r⦇current := current r',
                            TAs_state := TAs_state r',
                            REE_state := REE_state r',
                            TEE_state := TEE_state r',
                            system_time := system_time r',  
                            exec_prime := exec_prime r'⦈"

declare abstract_state_def and abstract_state_rev_def


section "Design level specification: function"
subsection "Module: IPC driver"

(*we assume that TEE's self-initalization is ok, thus no bound check here*)
definition fifo_create::"driver⇒fifo⇒fifo⇒driver"where
  "fifo_create d f1 f2 ≡ 
          d⦇tamgr_fifo := f1,
            svchost_fifo := f2⦈"


(*out_result is default to ZX_ERR_INTERNAL, represent whether out_params is valid, here ignore*)
definition Driver_Tamgr_get_fifo::"driver⇒fun_id⇒out_result⇒out_params⇒(out_result × out_params × RET)"where
          "Driver_Tamgr_get_fifo dri fun_id result param ≡ 
                        let call = zx_channel_call in
                          if call = False 
                                then (result, param, ZX_ERR_INTERNAL)
                          else 
                               (ZX_OKr, tamgr_fifo dri, ZX_OK)"


definition Driver_Svchost_get_fifo::"driver⇒fun_id⇒out_result⇒out_params⇒(out_result × out_params × RET)"where
              "Driver_Svchost_get_fifo dri fun_id result param ≡ 
                      let call = zx_channel_call in
                          if call = False 
                                then (result, param, ZX_ERR_INTERNAL)
                          else 
                               (ZX_OKr, svchost_fifo dri, ZX_OK)"

definition Driver_Get_rot_info::"driver⇒fun_id⇒out_result⇒out_params⇒(out_result × out_params × RET)"where
              "Driver_Get_rot_info dri fun_id result param ≡ 
                  (ZX_OKr, param , ZX_OK)"

typedecl Data (*from IPC driver to TA-mgr, e.g.openseesion anda its parameter*)

(*check the parameter tranfered from IPC driver to TA-mgr, e.g. openSession ands its data *)
(*including param check anda command id search. 
PS : it should be checked ina ta-mgr*)
definition check_Data::"Data⇒SMC_ERROR" where
      "check_Data data ≡ OPTEE_SMC_RETURN_OK"


definition param_init::"smc_params⇒Data⇒smc_params"where
      "param_init param data ≡ 
       let check_result = check_Data data in
                  if check_result = OPTEE_SMC_RETURN_EBADADDR
                      then param⦇a0 := 0, a1 := 4⦈
                  else if check_result = OPTEE_SMC_RETURN_EBADCMD
                      then param⦇a0 := 0, a1 := 5⦈
                  else
                      param⦇a0 := 0, a1 := 0⦈"

(*called by Ta-mgr/svchost*)
definition Driver_Write_smc ::"StateR⇒ReadSub⇒out_result⇒smc_params⇒(StateR × out_result × RET)" where
            "Driver_Write_smc s rs result smc ≡ 
                                let call = zx_channel_call;
                                    s1=(
                                      if rs=zx_mgr then
                                            s⦇IPC_driver:=
                                            ((IPC_driver s)⦇tamgr_data:=smc⦈)⦈
                                      else  s⦇IPC_driver:=
                                            ((IPC_driver s)⦇svchost_data:=smc⦈)⦈)
                                in
                                if call = False
                                    then (s,result, ZX_ERR_INTERNAL)
                                else
                                    (s1,ZX_OKr, ZX_OK)"
(*param1 = param_init param data*)


(*PS:this step is not shown in document, we added it to make it reasonable*)
(*called by ipc dirver, write and transfer message  to mgr/svchost*)
definition Driver_Read :: "StateR⇒smc_params⇒ReadSub⇒StateR" where
        "Driver_Read s smc rs≡(if rs=zx_mgr then
                               s⦇IPC_driver:=((IPC_driver s)⦇tamgr_data:=smc⦈)⦈
                          else s⦇IPC_driver:=((IPC_driver s)⦇svchost_data:=smc⦈)⦈)"  




section "Events"


datatype HypercallR =TEEC_INITIALIZECONTEXT TEE_NAME "TEEC_CONTEXT_TYPE option"

                |TEEC_FINALIZECONTEXT "TEEC_CONTEXT_TYPE option"
                |TEEC_OPENSESSION1 "TEEC_CONTEXT_TYPE option" "TEEC_SESSION_TYPE option"
                                TA_UUID_TYPE Connection_Method Connection_Data "TEEC_Operation option" "(MemBlock × TEEC_MEMREF_TYPE)"
                |TEEC_OPENSESSION2
                |TEEC_OPENSESSION3 SESSION_ID_TYPE
                |TEEC_OPENSESSION4 
                |TEEC_CLOSESESSION1 FD_TYPE "SESSION_ID_TYPE option" PARAMS_TYPE PARAMS_TYPE
                |TEEC_CLOSESESSION2
                |TEEC_CLOSESESSION3
                |TEEC_CLOSESESSION4
                |TEEC_INVOKECOMMAND1 "SESSION_ID_TYPE option"  TIMEOUT_TYPE COMMAND_ID_TYPE PARAMS_TYPE PARAMS_TYPE "MemBlock × TEEC_MEMREF_TYPE"
                |TEEC_INVOKECOMMAND2
                |TEEC_INVOKECOMMAND3
                |TEEC_INVOKECOMMAND4
                |TEEC_REGISTERSHAREDMEMORY TEEC_CONTEXT_TYPE  TEEC_SharedMemory
                |TEEC_ALLOCATESHAREDMEMORY TEEC_CONTEXT_TYPE  TEEC_SharedMemory
                |TEEC_RELEASESHAREDMEMORY TEEC_SharedMemory
                |TEE_OPENTASESSION1 
                |TEE_OPENTASESSION2
                |TEE_OPENTASESSION3 SESSION_ID_TYPE
                |TEE_OPENTASESSION4
                |TEE_INVOKETACOMMAND1 "MemBlock × TEEC_MEMREF_TYPE"
                |TEE_INVOKETACOMMAND2
                |TEE_INVOKETACOMMAND3
                |TEE_INVOKETACOMMAND4
                |TEE_CLOSETASESSION1
                |TEE_CLOSETASESSION2
                |TEE_CLOSETASESSION3
                |TEE_CLOSETASESSION4
                |TEE_CHECKMEMORYACCESSRIGHTS accessFlags  MemBlock  BUFFER_SIZE_TYPE
                |TEE_MALLOC BUFFER_SIZE_TYPE hint
                |TEE_REALLOC MemBlock BUFFER_SIZE_TYPE
                |TEE_FREE MemBlock


datatype SyscallR = Reserved

datatype EventR = hyperc' HypercallR|sys' SyscallR



end